es:ES, ff:FIFO, f2f+:F2F+-decls. R_dcdr  i:ff.Ce:EDec(ff.R(i,e)) 

latex

Definitions	x. t(x), P  Q, P & Q, , R_dcdr, t  T, x:A. B(x), x(s), F2F+-decls
Lemmas	event system wf, FIFO wf, F2F+-decls wf, bool wf, es-dtype wf, pi2 wf, top wf, snd-it wf, not wf, es-loc wf, Id wf, fifoS wf, fifoR wf, decidable wf, es-E wf, fifoC wf, pi1 wf